c formula generated with seed 8, probabilty values 0.414000 0.028000 0.503000 and clause ration 4.408889
c the planted solution is {1, 2, 3, 7, 9, 11, 14, 15, 16, 19, 20, 23, 24, 27, 28, 32, 33, 34, 35, 38, 39, 41, 42, 44, 45, 46, 50, 54, 56, 57, 58, 60, 70, 75, 76, 77, 78, 79, 80, 81, 83, 85, 86, 88, 93, 96, 99, 101, 102, 106, 112, 113, 114, 116, 117, 118, 119, 120, 121, 122, 125, 126, 128, 129, 130, 135, 136, 137, 139, 145, 146, 148, 150, 153, 156, 157, 161, 164, 166, 167, 170, 172, 174, 175, 176, 178, 179, 182, 184, 185, 187, 191, 192, 193, 196, 198, 199, 200, 201, 203, 204, 205, 206, 207, 209, 210, 211, 212, 214, 215, 219, 221, 223, 224, 225, 231, 233, 234, 237, 238, 239, 240, 241, 243, 244, 247, 249, 254, 256, 257, 260, 261, 264, 265, 271, 274, 277, 279, 282, 284, 286, 287, 293, 295, 296, 298, 299, 300, 302, 303, 305, 310, 315, 316, 317, 319, 321, 324, 325, 327, 333, 336, 337, 338, 339, 345, 347, 350, 351, 352, 353, 354, 357, 360, 361, 366, 367, 370, 374, 375, 378, 380, 381, 383, 386, 387, 388, 390, 393, 394, 396, 397, 401, 403, 405, 406, 408, 410, 412, 413, 416, 417, 420, 421, 424, 425, 426, 427, 429, 430, 431, 432, 434, 435, 436, 437, 438, 439, 441, 442, 443, 445}
p cnf 450 1984
-173 196 9 0
34 -256 59 0
-227 289 -205 0
-56 -325 -18 0
67 314 243 0
-189 412 170 0
377 -66 -24 0
245 304 -91 0
-127 259 -34 0
-152 213 -439 0
204 -123 176 0
-135 -76 70 0
-346 -382 50 0
-302 -96 277 0
354 364 143 0
-267 97 188 0
-91 412 -180 0
422 5 -18 0
423 324 -206 0
-69 308 364 0
-36 -403 -98 0
148 -161 235 0
-50 258 161 0
448 -330 -425 0
-272 344 106 0
-235 345 185 0
-163 -300 307 0
-62 -326 411 0
125 89 -210 0
391 -21 -198 0
247 430 360 0
-88 -339 -332 0
58 216 36 0
-418 350 -403 0
283 -247 -188 0
57 400 -60 0
364 271 -336 0
-13 -38 89 0
-360 371 420 0
146 -27 355 0
434 122 -444 0
10 -158 -137 0
-375 222 129 0
209 -108 129 0
-75 261 431 0
80 -222 219 0
301 353 -187 0
-64 332 -146 0
250 -56 -392 0
-396 107 42 0
-130 302 -166 0
376 201 -23 0
160 -73 55 0
-74 415 342 0
19 -424 -443 0
209 -207 87 0
-126 421 -271 0
-368 -278 -10 0
297 -283 185 0
-101 16 -271 0
19 192 325 0
317 146 -322 0
76 -335 -384 0
372 411 106 0
434 194 312 0
-391 -264 314 0
190 124 247 0
97 -402 30 0
-93 363 -371 0
330 -232 188 0
-328 -442 -420 0
-416 304 146 0
327 152 290 0
285 -409 -336 0
440 275 -290 0
91 -316 327 0
-68 -16 87 0
-270 -438 -325 0
-319 -19 120 0
-288 -439 -432 0
-47 147 -437 0
-35 -264 -61 0
-394 -119 -52 0
57 -323 374 0
285 328 -399 0
296 -310 47 0
-439 363 -251 0
-326 -442 433 0
130 88 375 0
-246 -69 112 0
-217 185 -342 0
-16 -248 -211 0
-425 -138 -230 0
-298 -359 -406 0
-250 -414 215 0
303 203 -181 0
157 -96 -9 0
-42 99 -182 0
-162 191 -323 0
333 -353 -63 0
200 -289 172 0
341 -121 78 0
-48 -72 -285 0
-377 -161 322 0
-248 -24 105 0
-144 159 -121 0
192 254 429 0
-56 -378 420 0
-222 231 178 0
-408 -398 174 0
-139 61 -132 0
-232 -407 -69 0
407 443 259 0
-86 39 251 0
33 3 77 0
-376 72 -50 0
-430 19 428 0
-3 -289 -145 0
191 97 -70 0
-16 -425 -208 0
-90 138 8 0
-285 429 256 0
392 -195 -436 0
343 -245 -86 0
-414 -341 -322 0
146 -175 253 0
-134 145 436 0
184 68 189 0
-275 119 9 0
228 342 -123 0
330 267 76 0
-25 223 -276 0
16 -113 -77 0
189 330 57 0
-283 -238 6 0
-228 335 -219 0
-395 -159 -22 0
-53 -85 -225 0
137 242 29 0
315 232 155 0
-337 403 -214 0
-97 -38 -239 0
-341 443 -267 0
-258 -190 -219 0
410 -215 358 0
78 -22 394 0
294 444 244 0
350 180 -401 0
-97 -67 203 0
-84 135 150 0
352 -419 -318 0
151 -399 -176 0
-335 -402 284 0
-407 -225 95 0
-105 12 51 0
347 -242 93 0
157 -447 -97 0
35 -84 56 0
412 -7 74 0
-431 -343 149 0
-390 277 418 0
-328 -212 -207 0
403 -26 -147 0
363 -280 -231 0
-228 -59 317 0
295 450 448 0
-197 364 313 0
-216 -215 329 0
-78 384 374 0
-48 408 350 0
362 -72 311 0
307 -43 269 0
55 328 11 0
-258 443 425 0
-286 88 33 0
261 117 76 0
-16 61 145 0
-140 322 394 0
-423 135 191 0
-295 78 94 0
387 -102 -125 0
-131 37 -255 0
-313 17 66 0
-405 -419 -305 0
338 -111 -242 0
-422 307 -209 0
38 84 450 0
-178 -277 325 0
-174 118 311 0
-283 -327 -243 0
96 -17 -113 0
90 3 356 0
-65 -391 112 0
-431 295 194 0
-214 113 -436 0
-353 -142 171 0
302 213 311 0
-381 98 129 0
381 -405 -235 0
323 215 216 0
-444 118 435 0
-146 271 -204 0
-250 -379 426 0
-23 260 202 0
180 -41 118 0
53 212 71 0
-394 35 -205 0
-253 -385 319 0
-87 286 -252 0
286 25 40 0
-351 22 122 0
-157 -258 -76 0
194 -54 210 0
-5 -70 -295 0
-446 317 310 0
213 156 -432 0
-36 -434 4 0
-439 -300 -131 0
211 329 63 0
-68 72 -299 0
261 322 -58 0
60 232 -79 0
196 -280 110 0
-448 260 113 0
374 420 287 0
219 102 -98 0
425 -421 309 0
278 308 -74 0
94 239 253 0
415 -188 -221 0
86 -385 -330 0
-103 -47 199 0
38 424 -409 0
-83 -1 327 0
-216 3 -63 0
415 -41 24 0
175 -149 200 0
-371 105 252 0
-301 229 -77 0
-165 -254 48 0
441 -17 -376 0
245 31 -115 0
168 -316 -340 0
-401 -22 306 0
-337 187 318 0
-444 -296 342 0
99 -206 107 0
294 8 -108 0
-78 -214 -450 0
-135 11 301 0
-291 -216 -259 0
212 103 -325 0
386 -105 176 0
191 211 234 0
-177 -281 -415 0
-133 -335 178 0
-252 316 421 0
-270 -331 93 0
424 -246 -30 0
240 -384 130 0
65 248 397 0
296 -51 -47 0
109 283 -253 0
340 284 72 0
-405 129 -7 0
-364 201 265 0
257 431 319 0
120 294 266 0
-167 154 60 0
-402 305 -323 0
22 -189 47 0
250 191 -14 0
203 -124 -141 0
289 125 -257 0
-77 201 92 0
16 -191 40 0
346 -257 -373 0
-73 -218 -104 0
-184 -227 406 0
32 223 413 0
-368 -84 -89 0
197 13 -82 0
-274 42 52 0
-121 -89 -338 0
-204 261 448 0
118 145 146 0
-298 352 -303 0
-86 -373 -445 0
-409 -158 353 0
198 342 -386 0
397 351 -108 0
384 344 352 0
-247 -76 -407 0
-191 357 -19 0
-176 -356 314 0
-228 -314 122 0
-381 132 393 0
-267 -439 36 0
271 -14 -412 0
163 40 -340 0
-183 363 141 0
412 -30 295 0
-169 32 -6 0
-144 192 249 0
384 352 200 0
-94 67 4 0
95 -394 347 0
391 -309 -215 0
-155 -9 -387 0
444 133 287 0
418 -307 163 0
-84 420 -415 0
-227 -301 -416 0
440 357 48 0
-162 -178 -203 0
-48 -360 -338 0
343 -16 -218 0
-107 18 318 0
-181 57 403 0
-275 -81 163 0
-116 354 -46 0
-30 234 -162 0
339 308 -167 0
-271 -409 22 0
-45 -119 -304 0
21 -132 -403 0
172 -422 99 0
-183 352 -229 0
237 434 420 0
44 -447 206 0
223 240 201 0
134 -52 -316 0
-391 -132 -173 0
-51 33 -322 0
361 -92 191 0
269 86 30 0
424 -62 -242 0
241 396 157 0
-109 -48 -180 0
41 -133 321 0
-275 22 84 0
296 -214 294 0
259 79 -206 0
-69 -13 -184 0
-306 -243 -182 0
-283 373 -161 0
-281 -267 360 0
15 -317 404 0
234 -298 364 0
-56 -129 -404 0
-337 -363 250 0
-269 -311 137 0
379 253 -180 0
18 -275 143 0
353 -435 358 0
-274 340 179 0
201 -202 306 0
-384 -443 259 0
-107 -266 333 0
-340 278 270 0
241 32 -250 0
185 332 -366 0
-59 189 -187 0
170 427 207 0
-77 163 -422 0
79 -344 -278 0
203 -340 254 0
135 438 317 0
-138 -210 152 0
154 186 -36 0
-17 52 -322 0
156 185 -62 0
250 255 -359 0
-69 442 201 0
219 -292 -22 0
-73 188 235 0
-56 288 256 0
-422 -141 244 0
-409 -97 -285 0
-168 -211 -271 0
-192 324 297 0
168 -298 -147 0
174 -55 -152 0
-8 -67 -37 0
39 -165 80 0
-348 -447 211 0
206 -231 124 0
431 178 -151 0
127 -410 -227 0
-363 -395 96 0
414 -387 -308 0
358 -52 278 0
-252 -171 -89 0
226 104 199 0
-306 -396 323 0
252 439 -19 0
327 -212 217 0
50 320 -319 0
71 -413 381 0
42 -422 321 0
146 85 -171 0
-388 448 -229 0
380 175 -312 0
292 -326 112 0
-125 184 392 0
301 -232 355 0
-264 -38 -301 0
-281 27 -318 0
-12 293 -329 0
-260 -311 -278 0
-67 215 -194 0
222 -394 370 0
-21 81 -377 0
346 314 23 0
92 -368 -57 0
48 135 -70 0
-245 156 170 0
333 90 -417 0
-373 -51 153 0
-108 -360 -117 0
244 -418 240 0
-259 182 93 0
-116 432 411 0
47 -4 -173 0
250 -16 361 0
249 299 101 0
-94 -113 359 0
238 -416 73 0
240 12 162 0
-180 157 -334 0
164 319 -330 0
-217 6 -176 0
281 123 -428 0
-128 -74 358 0
-241 24 -2 0
-218 192 -181 0
-42 -306 156 0
-43 -337 173 0
-289 -258 -87 0
366 208 450 0
275 -208 -118 0
-370 -300 -449 0
-144 -100 237 0
-415 -45 -319 0
-54 147 427 0
-29 -390 -445 0
-233 -373 363 0
-115 -286 -156 0
119 -125 400 0
-2 274 392 0
-348 -165 172 0
-355 -397 258 0
-364 -376 -155 0
360 -426 -324 0
57 254 -82 0
-311 -183 -344 0
361 442 210 0
-155 -307 16 0
19 381 224 0
-369 4 -243 0
-412 -298 157 0
-64 -6 -415 0
-54 15 -394 0
-370 -399 344 0
-174 272 -92 0
423 -131 -427 0
-287 -176 237 0
121 6 -233 0
-144 108 47 0
87 -293 406 0
178 -285 -447 0
146 -173 150 0
305 117 128 0
441 218 151 0
352 173 -260 0
100 -139 57 0
246 3 349 0
-207 299 -277 0
251 -325 -202 0
-72 387 112 0
61 -415 -420 0
-103 50 406 0
129 443 -270 0
169 -109 -383 0
227 345 87 0
402 46 -205 0
-239 -189 -413 0
118 410 -169 0
-73 260 -402 0
279 21 -174 0
130 228 -381 0
7 -5 -363 0
309 26 302 0
-143 -8 -280 0
-75 -253 123 0
-79 -265 80 0
363 117 43 0
-37 -71 182 0
237 299 -104 0
61 347 275 0
-433 -109 -414 0
220 379 117 0
-82 135 -222 0
-302 405 -27 0
306 446 -186 0
169 98 -250 0
-277 46 269 0
74 40 -48 0
163 -318 36 0
250 -127 -374 0
23 -390 -117 0
-441 32 422 0
-408 27 37 0
-195 205 -322 0
-360 -372 332 0
-352 275 -53 0
-357 34 -221 0
300 378 42 0
158 -215 303 0
29 85 152 0
-251 -162 396 0
-263 -25 87 0
-369 -361 -193 0
-84 246 -32 0
-38 296 -37 0
334 193 -204 0
257 -268 -288 0
336 -232 99 0
55 -170 -330 0
-374 25 -328 0
-89 189 186 0
328 205 389 0
249 409 -20 0
346 362 39 0
-424 -298 -433 0
203 139 206 0
253 415 -289 0
-268 205 150 0
-36 -25 24 0
215 -42 131 0
-234 9 270 0
146 20 -273 0
-95 -44 365 0
343 275 81 0
-338 237 -1 0
45 -324 -106 0
268 -369 -187 0
261 65 -237 0
-389 78 3 0
166 413 374 0
-95 -327 -174 0
-427 -88 316 0
180 -217 252 0
12 -440 -413 0
-409 -368 -37 0
294 -106 435 0
435 -426 190 0
47 281 -132 0
-173 -229 -67 0
143 -353 164 0
-395 -17 397 0
-272 203 324 0
-354 -112 166 0
17 339 -125 0
394 435 -285 0
-19 -336 76 0
-313 -229 145 0
21 -106 438 0
-67 -248 153 0
-211 147 -110 0
434 77 217 0
314 -386 119 0
254 336 238 0
140 435 307 0
290 -329 103 0
-356 421 -140 0
-410 -23 287 0
433 -308 -106 0
-329 -195 -392 0
397 -64 239 0
-116 300 -56 0
-36 -248 -422 0
285 280 -134 0
-44 86 65 0
-96 -198 -216 0
-119 -296 -186 0
-276 -314 -288 0
143 -302 -419 0
280 -252 328 0
198 -26 -124 0
-362 -396 334 0
-13 -18 274 0
136 -386 -167 0
392 286 190 0
422 -375 -97 0
-326 377 399 0
-444 -59 374 0
210 33 45 0
-23 -40 66 0
-299 -386 -330 0
-314 351 243 0
-274 -71 -327 0
152 -103 -393 0
426 22 -86 0
-210 46 314 0
-354 448 -262 0
216 -63 362 0
-140 -449 50 0
305 -142 184 0
289 -210 -371 0
301 261 -354 0
51 412 63 0
-32 182 -378 0
101 111 51 0
-29 134 115 0
-67 -345 -289 0
399 229 -365 0
332 72 -64 0
73 -138 18 0
229 -289 197 0
349 406 -233 0
442 -410 -161 0
-394 412 -209 0
316 1 212 0
-276 436 -285 0
-306 210 -151 0
325 319 390 0
-56 307 -411 0
105 -78 -363 0
-213 446 -305 0
-262 250 -327 0
181 -403 -248 0
-391 64 -1 0
-15 367 -58 0
-298 -108 -295 0
-62 -71 -382 0
-230 72 22 0
158 412 385 0
251 177 443 0
-251 -81 -102 0
301 -246 -70 0
-326 -25 -154 0
-26 376 189 0
183 -373 162 0
77 440 -129 0
173 371 -447 0
-281 63 55 0
305 -344 -97 0
-196 397 160 0
-168 210 261 0
-294 144 109 0
212 -130 -146 0
-193 132 -103 0
195 -220 55 0
-310 78 -187 0
164 47 25 0
-368 -113 67 0
-367 -23 -306 0
-50 272 394 0
-441 -414 -219 0
-226 -305 -298 0
-204 302 -46 0
64 371 421 0
-358 329 68 0
-392 -439 -129 0
-154 320 285 0
20 -25 397 0
44 200 -332 0
-275 -142 260 0
106 395 -435 0
-393 412 -445 0
292 47 88 0
333 3 -73 0
261 -294 -377 0
-251 -393 275 0
-84 -25 350 0
-319 -358 29 0
344 333 111 0
-405 241 -327 0
-292 217 349 0
441 102 -377 0
407 -124 -365 0
-63 -7 -304 0
-368 -59 166 0
-33 380 323 0
-95 82 -76 0
-377 232 74 0
339 89 222 0
-277 264 289 0
-67 -208 430 0
152 -125 3 0
416 -342 -409 0
125 -292 -349 0
256 449 -257 0
-89 237 -343 0
368 -253 -143 0
-399 -393 10 0
342 64 -94 0
-297 214 -418 0
-358 53 -387 0
41 323 -325 0
-266 -211 26 0
232 35 115 0
330 199 169 0
151 -390 -115 0
51 -43 202 0
301 -87 -83 0
332 231 -121 0
-27 -449 -265 0
-351 -8 103 0
253 -423 -161 0
-87 -186 112 0
337 -266 247 0
-154 -447 -253 0
-423 218 -448 0
-438 -1 -71 0
-437 376 396 0
253 -390 11 0
-339 -435 241 0
-92 -391 -316 0
87 215 423 0
-332 440 -264 0
393 -73 -141 0
215 -82 34 0
214 391 -15 0
380 204 130 0
289 406 -1 0
-207 296 -14 0
437 -155 -422 0
-304 89 180 0
132 -337 443 0
297 -200 -334 0
40 200 -345 0
-127 295 361 0
-304 3 113 0
150 -450 157 0
-211 229 -318 0
-418 -242 360 0
306 5 -217 0
178 -305 226 0
-334 -273 -90 0
-103 55 68 0
-78 11 266 0
-310 378 359 0
29 -405 101 0
375 -190 128 0
42 -78 120 0
-151 -237 -77 0
204 -360 266 0
-330 -369 32 0
-438 202 204 0
265 37 222 0
-17 410 -141 0
404 -11 113 0
-319 -204 -409 0
-445 -8 307 0
-30 -274 -238 0
-372 -146 232 0
-390 -139 219 0
187 75 430 0
-349 444 -99 0
378 156 86 0
-171 -418 435 0
121 -189 -186 0
407 379 -108 0
-114 -139 445 0
-204 273 -348 0
-245 152 -274 0
61 -71 294 0
-139 -319 -26 0
-383 203 -351 0
-134 130 172 0
-62 322 66 0
-351 -375 265 0
-411 -235 -141 0
229 -191 -289 0
236 -259 -182 0
64 125 -34 0
41 -55 222 0
-430 385 295 0
-425 -417 -103 0
-323 -130 -24 0
103 212 228 0
276 -312 -345 0
-63 57 42 0
-161 237 -239 0
-101 153 57 0
-302 179 269 0
-373 -339 440 0
-289 -356 -332 0
-216 -448 -173 0
374 -304 416 0
-195 -343 223 0
296 106 -102 0
321 -184 -166 0
-85 -156 -17 0
246 -74 -437 0
-348 159 235 0
-89 346 115 0
324 -389 -25 0
-286 241 -77 0
-274 51 350 0
-244 -6 173 0
-9 221 -90 0
387 138 -223 0
303 157 -159 0
-109 93 305 0
-231 -254 211 0
-251 -148 -412 0
-10 -298 -338 0
-139 -432 254 0
259 184 -406 0
412 -134 351 0
383 -440 298 0
204 124 -93 0
-72 -1 323 0
310 215 199 0
173 -108 -42 0
399 10 -25 0
281 213 166 0
-220 282 -281 0
-262 -37 -163 0
349 -386 56 0
375 331 89 0
2 -317 -246 0
202 -213 -338 0
403 -48 315 0
-5 446 389 0
-398 -247 -102 0
367 -45 -345 0
172 -253 319 0
-190 -83 132 0
-115 -152 351 0
-426 -382 266 0
-21 431 145 0
297 -58 -399 0
311 -151 -56 0
-425 174 -232 0
-417 -111 -291 0
170 -244 235 0
-391 364 -361 0
157 -103 -71 0
-4 -252 387 0
351 275 -279 0
57 -105 206 0
-205 -336 405 0
-94 -248 -93 0
230 244 373 0
-47 -43 -340 0
-328 -25 -71 0
158 285 -67 0
-146 -216 385 0
268 310 -347 0
-48 -165 -89 0
-442 53 -415 0
441 -188 -216 0
-172 56 -73 0
-184 61 -266 0
-88 402 148 0
-116 206 -136 0
17 348 -349 0
-293 -247 122 0
-287 -196 -449 0
-79 359 -43 0
360 -97 -124 0
26 395 -348 0
413 -201 -54 0
-295 390 251 0
106 -355 -273 0
333 418 -282 0
-88 235 347 0
-210 -382 -130 0
-300 -43 252 0
-155 351 321 0
-74 -28 -413 0
67 -82 -237 0
-247 -414 -24 0
-86 318 209 0
198 -420 398 0
-378 274 97 0
-11 -436 -202 0
276 -423 177 0
32 106 254 0
274 155 -193 0
163 -97 -166 0
158 -251 -135 0
-436 -121 -103 0
449 -277 -138 0
-69 336 -18 0
375 23 -124 0
-142 27 319 0
-259 421 357 0
-236 -400 -67 0
84 -43 -416 0
-368 351 -31 0
336 -68 -389 0
-53 -363 -226 0
-352 -412 243 0
-267 -226 58 0
129 359 400 0
-249 -6 341 0
-73 -238 183 0
2 88 192 0
398 304 -384 0
-238 -232 -146 0
-302 51 360 0
262 -300 3 0
61 269 -51 0
267 -289 -137 0
-129 -260 -245 0
-321 361 -214 0
-236 -241 -207 0
-11 -376 313 0
2 315 249 0
418 355 233 0
-22 115 -38 0
-76 205 447 0
-169 53 399 0
-201 -109 -85 0
449 -392 262 0
-240 -250 -443 0
395 -68 358 0
175 -264 -243 0
-63 275 335 0
370 -36 -154 0
174 -425 -77 0
-46 84 353 0
65 -300 -313 0
-26 384 -251 0
331 113 -315 0
203 62 -215 0
380 141 428 0
288 196 183 0
336 292 -139 0
-176 56 -436 0
254 156 421 0
125 121 233 0
89 265 -336 0
-287 91 1 0
370 204 -245 0
294 103 191 0
95 -37 -187 0
193 153 350 0
-267 141 250 0
-367 360 -361 0
376 416 365 0
-349 22 343 0
-325 -121 -67 0
131 -284 7 0
374 -404 -320 0
-186 416 -168 0
291 302 -431 0
102 -407 101 0
-292 -259 -365 0
-92 25 110 0
112 -13 -291 0
437 -161 -397 0
34 321 78 0
-253 375 -108 0
-387 5 176 0
-54 57 143 0
65 76 18 0
-143 -297 -398 0
52 93 17 0
51 52 249 0
88 390 -449 0
-209 43 352 0
-8 366 -181 0
-395 226 373 0
257 378 -422 0
232 -73 288 0
-147 132 -16 0
-138 229 251 0
218 -141 62 0
309 11 177 0
235 -182 56 0
156 -364 425 0
18 317 253 0
162 96 287 0
-184 -173 -156 0
140 191 -125 0
-353 213 -202 0
-83 -343 12 0
-15 -199 -362 0
199 -130 194 0
-316 -158 227 0
-253 440 131 0
-338 95 -255 0
382 410 143 0
-151 370 174 0
-142 287 88 0
-224 -231 -82 0
145 186 171 0
-207 353 -220 0
-164 168 -147 0
450 -424 247 0
54 -398 -245 0
-91 -371 401 0
432 -154 200 0
82 60 -117 0
-422 -334 -362 0
-282 -89 444 0
-278 -238 446 0
163 -36 -410 0
246 158 57 0
272 -283 -296 0
411 416 262 0
256 -141 193 0
378 223 39 0
-402 -171 24 0
80 172 -331 0
157 -69 -369 0
-328 -366 -416 0
62 115 -252 0
38 278 76 0
444 138 24 0
313 255 -202 0
438 -184 -295 0
294 -424 -253 0
147 -446 105 0
-259 -71 -104 0
36 -107 -442 0
388 267 -112 0
-365 -37 -235 0
-103 434 408 0
-90 -167 21 0
-359 -235 58 0
-93 223 263 0
-263 236 -77 0
410 436 15 0
-196 84 -251 0
-155 -75 152 0
413 -55 -220 0
185 -368 179 0
226 363 -270 0
-351 97 430 0
285 -71 97 0
-24 -342 127 0
-307 179 80 0
187 145 -286 0
401 -384 56 0
428 71 256 0
209 -178 -436 0
-395 -2 291 0
-352 -199 442 0
45 -259 316 0
398 313 254 0
124 -13 -408 0
33 303 -334 0
377 -213 74 0
392 -26 -391 0
-278 172 -444 0
-449 -235 20 0
52 101 415 0
-299 190 3 0
56 69 -321 0
287 317 46 0
54 -47 -108 0
411 -65 50 0
-103 -203 -254 0
-311 -197 -269 0
-353 115 -450 0
25 -169 246 0
338 229 -436 0
-217 294 283 0
301 -384 -86 0
337 114 -448 0
308 -440 42 0
-14 -250 -164 0
-307 83 -251 0
-132 -141 448 0
-145 367 -370 0
170 -379 -165 0
-94 323 -150 0
-22 -52 -10 0
-263 351 238 0
-37 153 170 0
-164 -245 332 0
213 319 217 0
177 -121 -332 0
315 -40 -368 0
210 -296 -420 0
-165 260 221 0
202 -335 -395 0
-348 192 135 0
149 -224 164 0
45 -423 -444 0
88 -193 28 0
334 -267 -38 0
99 -5 401 0
-171 -303 -438 0
-104 -63 256 0
162 185 -56 0
430 321 -97 0
-17 -128 348 0
250 376 -180 0
163 -215 16 0
-89 26 180 0
-129 13 -84 0
36 42 49 0
371 -246 -69 0
383 -254 -193 0
-193 429 -148 0
-68 413 137 0
114 347 429 0
-308 -255 -147 0
44 222 54 0
416 268 168 0
-384 431 139 0
428 -77 178 0
322 -16 -195 0
-280 -288 -314 0
415 -119 -36 0
-240 173 -21 0
-411 -265 138 0
154 163 44 0
234 -57 -14 0
314 -431 -30 0
-39 345 -241 0
255 -418 -303 0
96 365 -382 0
-181 293 429 0
-67 -50 423 0
-49 -364 244 0
-244 113 -396 0
428 418 244 0
-382 -161 -394 0
-72 -40 293 0
338 359 -337 0
98 -330 -219 0
-150 -268 -204 0
-110 241 321 0
-63 -423 -365 0
-132 -151 -65 0
249 4 -214 0
447 76 -112 0
-365 -342 -373 0
219 -89 -227 0
153 -368 195 0
-22 345 -326 0
222 57 194 0
390 119 -90 0
46 408 96 0
247 335 -164 0
-428 -68 374 0
54 88 -134 0
98 196 368 0
233 120 196 0
-439 60 -209 0
43 260 22 0
-445 -112 -67 0
125 -302 292 0
-186 437 -160 0
43 -11 -152 0
434 372 332 0
-19 -64 -93 0
-195 -261 -167 0
-345 -407 -7 0
-347 419 390 0
230 -189 -243 0
401 -206 -191 0
-165 -49 239 0
-332 -267 -107 0
247 299 101 0
115 309 -449 0
54 186 259 0
408 136 211 0
70 -81 402 0
293 151 372 0
217 -241 -318 0
14 431 -255 0
202 275 -144 0
-14 134 -306 0
70 50 -332 0
222 394 -104 0
-433 -43 -104 0
-376 190 115 0
-224 358 -362 0
145 212 -307 0
102 -208 421 0
-370 -402 -333 0
-424 6 -291 0
-20 159 -183 0
378 -169 -10 0
-51 261 -446 0
89 -408 -364 0
-214 5 -216 0
51 -125 -411 0
-167 -149 66 0
446 61 113 0
34 386 -422 0
-67 -303 395 0
-221 69 23 0
400 -336 401 0
449 326 257 0
226 408 299 0
189 -21 -287 0
314 -249 -307 0
178 106 265 0
-98 -342 153 0
22 -444 285 0
-123 55 73 0
334 -222 446 0
406 64 330 0
150 -47 -155 0
-439 234 51 0
-416 -305 221 0
150 -275 92 0
163 -375 -358 0
419 127 93 0
-24 427 415 0
124 396 -430 0
-364 244 -194 0
-112 -224 -49 0
407 176 -412 0
229 64 174 0
89 62 378 0
-127 412 339 0
130 -53 366 0
284 298 277 0
-318 -176 -327 0
-360 -24 274 0
97 -84 163 0
29 282 -122 0
28 57 -94 0
-363 20 -343 0
98 143 390 0
271 375 191 0
-51 210 -331 0
-244 80 229 0
-369 448 449 0
-268 -342 313 0
154 -226 308 0
-426 21 15 0
-433 -387 220 0
389 -429 -440 0
-58 -424 -258 0
211 -147 -385 0
-378 -127 -214 0
215 69 -44 0
-309 -282 -396 0
-261 -402 105 0
-256 -301 332 0
405 155 -317 0
-135 241 -191 0
-26 -398 -22 0
-170 -327 -358 0
214 155 -432 0
264 272 -215 0
306 27 74 0
-78 384 86 0
282 -440 -222 0
-114 296 140 0
-425 -392 -214 0
339 329 373 0
16 446 -361 0
-151 117 256 0
-414 -366 294 0
-97 -294 -159 0
265 -387 97 0
-423 354 -51 0
265 348 245 0
-199 -40 384 0
420 -210 342 0
173 337 -70 0
196 299 175 0
26 -235 88 0
338 406 -313 0
-65 388 389 0
-397 368 -252 0
-178 -95 -387 0
391 -262 190 0
-17 161 -144 0
-135 133 333 0
-414 443 -226 0
369 -338 -415 0
-140 247 187 0
315 244 -181 0
194 -228 -367 0
-294 388 179 0
200 -261 -238 0
-199 -25 342 0
411 -25 -142 0
-148 49 -97 0
-325 -144 -429 0
245 -17 -211 0
95 -61 -198 0
78 -332 -213 0
101 -6 -230 0
-84 -449 19 0
78 -356 256 0
425 -329 85 0
15 -389 380 0
-235 238 134 0
218 347 268 0
-365 -118 -237 0
53 88 66 0
273 96 400 0
-435 400 137 0
439 312 68 0
-351 180 157 0
440 -246 158 0
-136 -423 -396 0
73 -98 -206 0
-361 -434 393 0
20 -296 -114 0
-393 59 432 0
431 214 191 0
274 368 398 0
-327 -292 -256 0
57 163 -316 0
-324 -95 -200 0
243 160 -184 0
150 -392 -255 0
-178 -115 40 0
143 -151 -303 0
408 425 317 0
88 -119 -296 0
-345 362 -183 0
426 16 147 0
-419 41 88 0
-250 186 -293 0
-117 -253 -11 0
142 -247 -297 0
-110 442 417 0
-62 401 437 0
-10 372 -60 0
-49 -265 341 0
134 -81 -186 0
-418 -263 -100 0
-242 -126 -374 0
-63 -291 -262 0
2 -100 244 0
-312 434 300 0
361 -219 -221 0
364 157 -176 0
-266 325 167 0
183 94 412 0
-203 168 -304 0
-99 171 106 0
-73 -14 -416 0
230 -273 -155 0
-298 119 -56 0
-134 -305 -443 0
275 74 209 0
153 -158 -216 0
260 -447 192 0
-26 -367 154 0
5 -325 -31 0
-123 135 -235 0
-337 355 -25 0
151 -10 64 0
294 -68 84 0
392 -408 -365 0
144 220 360 0
61 279 -176 0
433 -105 313 0
-89 -397 -122 0
-443 124 170 0
60 -394 5 0
-194 68 -121 0
-232 429 -334 0
-368 -68 -217 0
120 158 377 0
-297 161 38 0
-406 -195 -139 0
-6 421 425 0
-127 373 185 0
439 208 -100 0
-28 -170 24 0
20 -356 420 0
-367 145 385 0
88 275 -212 0
-340 -100 70 0
-171 -214 -438 0
-260 -275 -442 0
265 -230 -169 0
244 53 -70 0
208 255 -344 0
-51 -319 -75 0
-68 270 -42 0
175 -93 389 0
325 212 7 0
204 418 31 0
-382 -20 -175 0
431 329 -212 0
317 -184 -410 0
-257 309 421 0
-388 376 -25 0
9 361 -4 0
291 400 -236 0
-174 182 -420 0
-378 130 -317 0
-229 277 44 0
-220 269 94 0
-220 166 -4 0
-202 -159 79 0
381 109 -316 0
-59 -218 -369 0
190 -216 202 0
444 -62 -344 0
317 -355 -25 0
373 313 175 0
97 44 138 0
-62 12 112 0
-315 -330 332 0
-323 -147 -262 0
-165 -437 -327 0
438 -97 352 0
316 -207 -300 0
42 303 430 0
-236 -224 -244 0
150 -345 -136 0
231 205 424 0
322 -14 357 0
48 -38 170 0
-42 -386 -311 0
363 439 335 0
175 -23 323 0
194 377 206 0
230 259 261 0
88 -150 181 0
259 14 -138 0
-268 -398 354 0
306 295 419 0
263 331 264 0
425 24 -74 0
22 -134 -96 0
231 413 128 0
-65 -146 270 0
-43 -40 201 0
219 -213 -82 0
216 184 -296 0
179 390 302 0
106 24 120 0
107 330 176 0
-185 -274 -21 0
-92 -43 -132 0
287 -368 -246 0
-370 -25 236 0
-87 -381 -367 0
202 -8 -412 0
448 312 -73 0
-367 233 -277 0
42 -355 -283 0
-265 321 446 0
-111 224 319 0
353 -242 -173 0
-357 -40 -270 0
-416 -255 -277 0
389 -263 -337 0
-223 403 -271 0
42 -273 79 0
66 -285 -357 0
104 55 -348 0
-162 274 337 0
352 -307 -104 0
-215 -68 -421 0
-373 -67 -63 0
-190 289 -239 0
-117 61 357 0
34 -66 45 0
4 -89 292 0
-129 147 83 0
-364 130 85 0
-419 22 152 0
39 443 118 0
278 -152 69 0
-12 195 363 0
322 84 287 0
417 -142 60 0
134 -140 16 0
131 34 -166 0
-62 130 247 0
-141 330 -212 0
7 415 226 0
-421 155 375 0
-389 436 77 0
122 219 -84 0
-48 -370 341 0
-27 11 138 0
313 349 209 0
54 -259 -22 0
-153 5 -362 0
-401 -416 -71 0
137 -335 139 0
317 -348 214 0
364 -133 -196 0
-159 336 -68 0
-67 -417 342 0
165 312 -418 0
202 100 -4 0
86 17 362 0
-122 69 215 0
-374 64 357 0
-138 -434 -148 0
241 355 -114 0
-87 -3 275 0
-370 -310 435 0
215 -263 -253 0
-364 241 -258 0
341 -393 199 0
-150 343 -246 0
263 -317 231 0
-155 -200 -75 0
-330 172 219 0
-124 -323 39 0
121 -258 -171 0
67 318 -373 0
160 14 -241 0
-428 -154 -440 0
-259 322 197 0
-274 -365 149 0
408 -177 316 0
-314 325 -414 0
-435 356 88 0
-425 296 -214 0
72 114 308 0
-64 -126 173 0
-127 -378 343 0
-248 -25 -344 0
-372 206 -4 0
177 -197 63 0
369 -386 370 0
139 167 -398 0
-24 -53 13 0
-190 -179 -396 0
208 239 -58 0
321 -314 -414 0
108 254 -137 0
-348 -342 -334 0
427 -157 304 0
213 -334 331 0
243 196 -154 0
-204 -181 -145 0
-140 -164 -327 0
-324 280 -419 0
-237 165 -10 0
-1 -13 -170 0
349 -262 407 0
-34 108 -197 0
271 -166 250 0
-209 387 -300 0
-198 158 1 0
1 -194 -269 0
-294 -115 -4 0
12 444 -363 0
49 -127 -357 0
435 -210 -120 0
-73 207 303 0
433 -199 381 0
354 -159 -40 0
-23 47 -6 0
-310 -378 -162 0
282 83 354 0
-317 390 -357 0
447 -241 -364 0
366 120 244 0
201 -388 169 0
224 78 -433 0
-389 -42 399 0
-20 330 14 0
-122 -276 309 0
71 330 -30 0
276 -97 66 0
-266 424 -18 0
-409 -231 47 0
195 428 -40 0
420 -90 -61 0
-305 75 245 0
149 433 394 0
-279 147 -402 0
30 -139 -275 0
95 -14 81 0
440 283 310 0
121 -178 348 0
252 -233 -395 0
-80 127 41 0
-226 173 232 0
111 208 -169 0
145 -299 26 0
116 -129 82 0
125 -440 182 0
-215 -179 -275 0
12 126 262 0
179 -100 -4 0
-334 297 69 0
441 -406 -86 0
-119 -198 412 0
-12 161 -340 0
178 -32 152 0
308 386 -333 0
421 -182 -119 0
350 -189 -322 0
332 172 -115 0
285 -64 -397 0
-322 -186 78 0
354 352 -66 0
-444 409 -434 0
-437 -388 310 0
274 264 -124 0
-104 90 -325 0
-64 303 -309 0
-127 -172 208 0
343 -229 313 0
-270 -250 -180 0
227 -378 305 0
435 422 95 0
-449 416 104 0
-348 -106 -211 0
83 -79 -368 0
254 -43 -329 0
235 -339 16 0
280 -387 -259 0
-342 36 62 0
-314 -52 396 0
-229 134 328 0
448 -342 355 0
76 -82 -373 0
25 -410 -52 0
-445 -112 -371 0
-161 419 -111 0
102 391 399 0
378 -411 -392 0
349 -164 200 0
128 -372 45 0
307 277 250 0
63 90 -342 0
229 50 -117 0
342 -257 -407 0
242 -240 -154 0
320 -153 16 0
-208 326 171 0
-417 -77 238 0
325 -96 -112 0
53 -416 192 0
-141 -419 412 0
-9 -422 -408 0
8 -263 110 0
-10 230 152 0
-76 110 -355 0
352 318 306 0
58 450 162 0
2 400 -15 0
449 -448 -302 0
-343 -302 280 0
279 -302 -408 0
-395 204 88 0
171 335 153 0
84 99 450 0
425 351 -359 0
-155 440 -15 0
-261 380 68 0
245 6 -22 0
-130 444 174 0
-106 365 -269 0
59 430 180 0
85 -206 309 0
-412 -21 -338 0
48 66 439 0
-212 433 117 0
434 -64 -419 0
-356 235 -9 0
54 -8 -250 0
214 180 -357 0
231 411 -139 0
305 419 232 0
158 43 -289 0
339 -48 -358 0
328 -248 90 0
-323 312 159 0
-166 292 243 0
-141 -422 -376 0
41 -239 248 0
375 234 -175 0
-6 -148 246 0
181 -77 339 0
-246 317 256 0
-305 138 397 0
-65 8 140 0
400 -403 3 0
130 -114 53 0
77 -94 -129 0
-272 -336 -260 0
184 -134 417 0
-410 181 204 0
286 -329 -133 0
57 436 -132 0
-105 -350 36 0
141 -83 172 0
-241 84 -8 0
403 -158 -220 0
-50 211 -38 0
-36 326 80 0
-301 -200 131 0
125 12 -19 0
-140 -163 284 0
65 -150 39 0
358 349 35 0
-82 384 -317 0
439 -82 83 0
-340 321 293 0
-323 398 372 0
-261 -344 226 0
53 139 -50 0
-450 347 -73 0
244 66 343 0
-72 15 387 0
297 -380 -141 0
-107 -318 56 0
-293 174 376 0
187 -85 -336 0
130 -73 420 0
206 -315 71 0
-317 247 -324 0
343 139 297 0
-444 -217 -99 0
-391 -167 -182 0
321 -230 -376 0
191 431 19 0
-222 146 198 0
379 258 -162 0
257 -290 145 0
-78 117 -333 0
131 2 18 0
408 31 -360 0
-31 -268 375 0
-195 -280 -448 0
86 114 225 0
-339 -126 157 0
61 66 -190 0
-15 -141 419 0
-416 385 413 0
387 435 -292 0
163 -56 196 0
-181 415 -78 0
47 369 421 0
-124 -275 -30 0
-137 209 169 0
-46 -102 436 0
-331 424 129 0
103 382 54 0
259 -356 -242 0
414 199 -393 0
366 -291 247 0
435 -174 31 0
-386 -76 196 0
-60 211 -79 0
-1 117 -257 0
122 -121 314 0
-385 435 295 0
-360 38 105 0
-295 -429 211 0
-391 -307 -262 0
176 164 106 0
201 -285 -48 0
-387 353 -126 0
-17 -322 225 0
-31 373 362 0
441 356 -304 0
12 296 228 0
-235 -246 191 0
178 -224 276 0
422 133 -105 0
271 32 -116 0
-423 436 -259 0
35 143 -429 0
284 417 -373 0
-220 97 -225 0
-143 107 103 0
-17 130 393 0
286 -442 -300 0
27 188 5 0
-31 -95 305 0
-259 -408 -79 0
19 -383 227 0
-273 -424 43 0
193 -317 -417 0
-366 -290 82 0
115 152 -311 0
-104 -314 -217 0
-238 -305 -177 0
373 63 -53 0
-275 -256 253 0
331 -98 356 0
60 -314 -141 0
-1 -213 -403 0
405 147 -233 0
77 148 24 0
371 -402 -324 0
334 -195 235 0
-331 239 -66 0
-86 171 -281 0
380 -36 41 0
-147 -285 -411 0
-110 -236 254 0
-181 -69 -100 0
-54 -328 213 0
389 287 229 0
15 -94 445 0
164 282 -371 0
-208 -247 404 0
-54 -108 127 0
-277 -315 118 0
-368 173 18 0
278 -52 230 0
56 179 327 0
314 -321 117 0
23 29 -58 0
-226 1 130 0
-269 -61 298 0
224 -346 20 0
-40 -433 -225 0
-152 -331 174 0
41 -295 -310 0
-404 -231 94 0
-73 -276 75 0
329 418 315 0
309 -323 -393 0
139 311 -119 0
327 -250 317 0
363 -209 -236 0
-39 -443 -448 0
74 126 -321 0
-207 332 -142 0
-13 -101 384 0
204 -190 106 0
-201 -177 -416 0
73 161 -80 0
-273 432 -140 0
-222 250 -325 0
-170 291 -289 0
297 48 -8 0
331 251 441 0
386 -265 -281 0
406 424 -92 0
-365 -196 138 0
-344 94 127 0
318 344 41 0
183 -335 -157 0
-76 58 -206 0
-72 -279 334 0
325 62 -179 0
-385 127 74 0
274 -116 -224 0
119 327 239 0
376 -126 244 0
318 -153 366 0
224 -1 -85 0
88 438 112 0
-172 -384 -354 0
-360 301 -331 0
376 -448 -130 0
340 288 249 0
-216 -324 152 0
8 235 -133 0
430 4 -157 0
58 153 137 0
-110 -91 120 0
414 434 292 0
359 -39 -115 0
-142 229 -366 0
-321 -307 -357 0
-186 326 423 0
375 185 441 0
234 28 366 0
274 -184 -96 0
-388 -113 -63 0
297 228 -385 0
208 272 435 0
-382 70 -418 0
250 -353 -372 0
-191 -305 -235 0
-263 -41 -441 0
264 242 -77 0
-47 -312 439 0
-121 286 23 0
-172 -161 -26 0
-151 -338 12 0
325 117 310 0
220 -146 430 0
-185 176 64 0
-449 -430 -198 0
-94 -13 201 0
397 280 162 0
91 304 207 0
375 -73 445 0
323 -441 88 0
-312 178 -59 0
-71 226 -212 0
329 31 324 0
443 -94 -391 0
-210 153 -166 0
-93 -433 -403 0
-306 50 -47 0
-203 54 152 0
-398 -358 -25 0
-144 -56 -38 0
-255 437 -109 0
241 -382 380 0
393 -422 9 0
166 -398 101 0
-427 249 -119 0
95 -266 -179 0
437 376 -145 0
332 67 -65 0
-43 -370 -441 0
-209 -69 406 0
183 260 -58 0
41 -154 -245 0
22 325 142 0
-22 24 139 0
410 415 160 0
-255 -388 82 0
417 -353 5 0
213 312 215 0
234 -308 -12 0
25 -126 -154 0
-317 21 106 0
-33 -21 -256 0
-196 -208 -221 0
306 357 -337 0
137 2 279 0
132 -389 -88 0
87 381 71 0
227 -389 115 0
405 307 -390 0
-217 -46 428 0
-131 37 -78 0
201 -260 395 0
45 -300 -156 0
-406 146 404 0
279 295 -95 0
-90 -35 277 0
257 -228 166 0
-180 149 72 0
378 48 304 0
-415 -181 -272 0
-356 175 28 0
388 -154 32 0
-130 -53 377 0
383 -100 -69 0
-231 243 21 0
304 -78 35 0
-8 19 -36 0
105 -182 -162 0
-6 230 239 0
-449 -343 -218 0
-141 173 40 0
286 396 201 0
202 -440 73 0
170 204 240 0
160 -372 216 0
-302 43 42 0
-221 256 358 0
46 -84 -369 0
124 -281 -317 0
-179 411 70 0
-309 -59 -91 0
190 241 53 0
-290 121 -449 0
-213 -348 -51 0
265 65 143 0
437 -174 115 0
-256 -380 -97 0
-103 -218 -144 0
282 240 401 0
42 61 29 0
74 429 260 0
257 -232 256 0
-46 -131 13 0
-54 -362 63 0
-432 235 170 0
-40 380 201 0
-401 85 -156 0
362 335 -111 0
423 65 146 0
-365 277 -448 0
155 -50 -89 0
449 387 95 0
-294 -196 152 0
430 91 -210 0
-349 -152 253 0
-108 16 11 0